module ExtendedLambdaCase where

data Bool : Set where
  true false : Bool

data Void : Set where

foo : Bool → Bool → Bool → Bool
foo = λ { x → λ { y z → {!!} } }

module parameterised {A : Set}(B : A → Set) where

  data Bar : (Bool → Bool) → Set where
    baz : (t : Void) → Bar λ { x → {!!} }

  -- with hidden argument
  data Bar' : (Bool → Bool) → Set where
    baz' : {t : Void} → (t' : Void) → Bar' λ { x' → {!!} }


baz : Bool → {w : Bool} → Bool
baz = λ { z {w} → {!!} }

another-short-name : {A : Set} → (A → {x : A} → A → A)
another-short-name = {! λ { a {x} b → a } !}

f : Set
f =  (y : Bool) → parameterised.Bar {Bool}(λ _ → Void) (λ { true → true ; false → false })
